T:Type, P:((T List)prop{i:l}).
(L:(T List). decidable(P(L)))
 (L:(T List). 
 P(L)
  (L':T List
  ((iseg(T; L'; L)  P(L')  (L'':(T List). iseg(T; L''; L')  P(L'')  (L'' = L'))))) 

latex

Definitions

b, null(as), prop{i:l}, guard(T), ge(i; j), ||as||, decidable(P), P  Q, , A  B, A, False, P  Q, x:A. B(x), P  Q, iseg(T; l1; l2), x:A. B(x), x(s), t  T, x. t(x), P  Q, P  Q, True, last(L), A c B, sq_type(T), append(as; bs), T

Lemmas

cons iseg, squash wf, append wf, iseg append iff, iseg weakening, iseg append0, member wf, cons one one, iseg transitivity, last wf, length append, iseg length, decidable-exists-iseg, last lemma, assert wf, true wf, assert of null, implies functionality wrt iff, all functionality wrt iff, and functionality wrt iff, iseg wf, null wf2, iseg nil, null wf, decidable assert, length wf1, non neg length, le wf, nat wf, decidable wf, nat properties, ge wf